When practicing present day techniques, it is necessary to check the truth values for each assignment (interpretation) of 1 and 0 to the variables included in a formula.
The so-called resolution method can also be used in the case of simple systems. This method involves re-writing the original formula to a logic equivalent formula consisting of a number of parts which are mutually compared in accordance with the so-called resolution rule. When making a comparison between, for instance, an expression which contains A and an expression which does not contain A, this rule requires the formation of a new expression, a resolvent, which contains neither A nor not A. The concept is to find an expression which contains solely A and an expression which contains solely not A, wherewith when a comparison is made between these two expressions, there is formed an empty resolvent, which is the one sought.